A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))), e:E.
((e  (I|p)))  (((e  I)) & P(e)) 

latex

Definitions	x:A. B(x), x(s), P & Q, b, f(a), x:A  B(x), P  Q, P  Q, P  Q, x:AB(x), x. t(x), E, Dec(P), Type, , Top, left + right, ES, e  X, (I|p), AbsInterface(A)
Lemmas	iff functionality wrt iff, can-apply-p-restrict